|
In propositional calculus and proof complexity a propositional proof system (pps), also called a Cook–Reckhow propositional proof system, is system for proving classical propositional tautologies. == Mathematical definition == Formally a pps is a polynomial-time function ''P'' whose range is the set of all propositional tautologies (denoted TAUT).〔 If ''A'' is a formula, then any ''x'' such that ''P''(''x'') = ''A'' is called a ''P''-proof of ''A''. The condition defining pps can be broken up as follows: * Completeness: every propositional tautology has a ''P''-proof, * Soundness: if a propositional formula has a ''P''-proof then it is a tautology, * Efficiency: ''P'' runs in polynomial time. In general, a proof system for a language ''L'' is a polynomial-time function whose range is ''L''. Thus, a propositional proof system is a proof system for TAUT. Sometimes the following alternative definition is considered: a pps is given as a proof-verification algorithm ''P''(''A'',''x'') with two inputs. If ''P'' accepts the pair (''A'',''x'') we say that ''x'' is a ''P''-proof of ''A''. ''P'' is required to run in polynomial time, and moreover, it must hold that ''A'' has a ''P''-proof if and only if it is a tautology. If ''P''1 is a pps according to the first definition, then ''P''2 defined by ''P''2(''A'',''x'') if and only if ''P''1(''x'') = ''A'' is a pps according to the second definition. Conversely, if ''P''2 is a pps according to the second definition, then ''P''1 defined by : (''P''1 takes pairs as input) is a pps according to the first definition, where is a fixed tautology. 抄文引用元・出典: フリー百科事典『 ウィキペディア（Wikipedia）』 ■ウィキペディアで「Propositional proof system」の詳細全文を読む スポンサード リンク
|